[ty] Intersection simplifications with gradual generic specializations#26365
Draft
sharkdp wants to merge 8 commits into
Draft
[ty] Intersection simplifications with gradual generic specializations#26365sharkdp wants to merge 8 commits into
sharkdp wants to merge 8 commits into
Conversation
Typing conformance resultsNo changes detected ✅Current numbersThe percentage of diagnostics emitted that were expected errors held steady at 94.47%. The percentage of expected errors that received a diagnostic held steady at 89.19%. The number of fully passing files held steady at 95/134. |
Memory usage reportMemory usage unchanged ✅ |
|
| Lint rule | Added | Removed | Changed |
|---|---|---|---|
invalid-return-type |
2 | 0 | 0 |
unused-type-ignore-comment |
0 | 2 | 0 |
invalid-argument-type |
1 | 0 | 0 |
| Total | 3 | 2 | 0 |
Raw diff:
psycopg (https://github.com/psycopg/psycopg)
+ psycopg/psycopg/rows.py:145:12 error[invalid-return-type] Return type does not match returned value: expected `type[tuple[object, ...]] & type[NamedTupleLike]`, found `<class 'Row'>`
+ psycopg/psycopg/types/composite.py:514:12 error[invalid-return-type] Return type does not match returned value: expected `type[tuple[object, ...]] & type[NamedTupleLike]`, found `<class '<unknown>'>`
static-frame (https://github.com/static-frame/static-frame)
- static_frame/core/quilt.py:856:58 warning[unused-type-ignore-comment] Unused blanket `type: ignore` directive
- static_frame/core/quilt.py:862:46 warning[unused-type-ignore-comment] Unused blanket `type: ignore` directive
+ static_frame/test/unit/test_quilt.py:2111:45 error[invalid-argument-type] Argument to bound method `Quilt._axis_tuple` is incorrect: Expected `(type[tuple[object, ...]] & type[NamedTupleLike]) | None`, found `<class 'tuple'>`a15c984 to
13da00f
Compare
sharkdp
commented
Jun 29, 2026
Comment on lines
+413
to
+414
| static_assert(is_equivalent_to(type[P] & ~type[Any], type[P] & ~type[Never] & Any)) | ||
| static_assert(is_equivalent_to(~type[Any] & type[P], type[P] & ~type[Never] & Any)) |
Contributor
Author
There was a problem hiding this comment.
type[Never] is probably Never? So ~type[Never] could be removed from the intersection. It seemed orthogonal to the PR here, so I left it for now.
Member
There was a problem hiding this comment.
type[Never]is probablyNever?
Yup
13da00f to
7143abd
Compare
ecbba11 to
b534fbe
Compare
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
In
isinstance(..., C)andTypeIs[..]narrowing, we currently intersect with the top materializationTop[C[Unknown]]of a generic typeC. If we want to relax that to an intersection withC[Unknown]directly, then we will not just see intersections likeC[P] & C[Unknown]in theifbranch, we'll also see intersections likeC[P] & ~C[Unknown]in theelsebranch. If we don't simplify/transform these intersections further, we are currently unable to infer that the bottom materialization of something likelist[str] & ~list[Unknown]isNever1. So here, we implement the following intersection transformation:In this form, due to the intersection with a plain
Unknown, it is now obvious to ty that the gradual type extends all the way down toNever.I realize that the type on the right hand side doesn't look better, but it is much easier to reason about. Also, for some specific
C's, the~Bottom[C[Unknown]]may simplify toobject, so it falls out of the intersection. For example, I believe we could further simplifytype[P] & ~type[Unknown] = type[P] & Unknownin a follow-up.In addition, we also implement these transformations that we have derived before:
Ecosystem
A few new diagnostics since we remove a TODO type for intersections of
type[..]. All new diagnostics are true positives (they all have suppression comments for other type checkers).Test Plan
isinstancenarrowing #26361Footnotes
We might actually be able to infer that if we explicitly asked for the bottom materialization of that type. But when accessing attributes/methods on the type, we don't explicitly perform that operation. Instead, we iterate over the intersection elements and combine the attribute types. ↩